ESAtomAxiom{i:l}(T;V)
== (i, x:Id. AtomFree(Type;T(i,x))) & (i:Id, k:Knd. AtomFree(Type;V(i,k))) 

latex

---

clarification:

ESAtomAxiom{i:l}
ESAtomAxiom(T; V)
== (i:Id, x:Id. AtomFree(Type{i};T(i,x))) & (i:Id, k:Knd. AtomFree(Type{i};V(i,k))) 

latex

Definitions	P & Q, Id, x:A. B(x), Knd, AtomFree(T;x), Type, f(a)
FDL editor aliases	ESAtomAxiom